The present application relates generally to an improved data processing apparatus and method and more specifically to mechanisms for abstraction for arrays in integrated circuit models.
Systems with arrays are difficult to verify by model checking because arrays introduce many state variables and have complex addressing logic. In many cases, there is regularity in the way a system accesses its arrays. It is often possible to use such regularity to find a system with smaller arrays, such that correctness of the system with the smaller arrays implies correctness of the original system. This is the basic idea of array abstraction.
Large arrays are a barrier to verifying many designs. Arrays are not a niche; many units have arrays. Recently developed algorithms reason without fully expanding arrays into a bit-level model.
Most previous approaches to array abstraction create smaller models through an iterative process of abstraction and refinement. These approaches maintain an abstract model that is sound. If a correctness property holds in the abstract model, the original model also has the correctness property. If the abstract model fails to have the correctness property, the solution refines the abstract model. Refinement is the process of analyzing executions on which the correctness property fails and constructing a new model that does not have these executions. Abstraction refinement is an iterative process that may take many steps to prove or disprove a correctness property.
Some previous approaches use bounded abstraction. For bounded model checking, one models a small number of time steps and only models the addresses that are accessed in the bounded interval. An array accesses only a small number of addresses in a bounded interval. A bounded abstract model size depends on the number of time steps. This approach may result in many time steps to prove a correctness property by induction.
Another approach provides unbounded abstraction by building an abstract model by abstraction-refinement. This approach chooses modeled addresses non-deterministically. Modeled addresses have normal array semantics. For unmodeled addresses, reads return a non-deterministic value. The approach over-approximates the behavior of the original system. This approach provides conservative abstraction for safety properties. Each modeled address is characterized by a constant latency, which is the number of clock cycles from the time data is read from an array until data affects the output. The method cannot reduce the size of arrays in designs with unbounded latency, such as designs that read data from an array and use it after an unbounded interval or designs with clock gating.